package model.cnf;

import java.io.BufferedReader;
import java.io.File;
import java.io.FileInputStream;
import java.io.FileOutputStream;
import java.io.IOException;
import java.io.InputStream;
import java.io.InputStreamReader;
import java.io.RandomAccessFile;
import java.util.ArrayList;
import java.util.List;
import java.util.Scanner;

/**
 * <p>
 * A implementation of {@link CNF} using only the file associate to it.
 * </p>
 * <p>
 * Represent a CNF but don't store it in memory, it only check the number of clause and var. Every
 * access will cause to read in the file so FileCNF are less efficient for I/O operation than
 * MemoryCNF for example but most of the time you don't need to modify them, FileCNF use really less
 * memory and are used by default in general.
 * </p>
 * 
 * @author GRONOWSKI Stephane svan001@aol.com
 * 
 *         igsat 2010
 * 
 */
public class FileCNF extends CNF {

	public static final int		SIZE_BUFFER	= 4096;

	private RandomAccessFile	file;
	/* the line where the real CNF begin (after number of clause and var) */
	private int					begin		= 1;

	/**
	 * Create a new CNFile.
	 * 
	 * @param CNFfile
	 *            the pathname of the file.
	 * @throws IOException
	 *             if error with the file.
	 */
	public FileCNF(String CNFfile) throws IOException {

		this.CNFfile = new File(CNFfile);
		if (!this.CNFfile.isFile())
			throw new IllegalArgumentException();
		check();
	}

	@Override
	public File export(String cnf, File directory) {
		File tmp = null;
		try
		{
			tmp = new File(directory, cnf);
			tmp.createNewFile();

			FileInputStream read = new FileInputStream(CNFfile);
			try
			{
				FileOutputStream write = new FileOutputStream(tmp);
				try
				{
					byte[] tab = new byte[SIZE_BUFFER];
					int nbread;
					while ((nbread = read.read(tab)) > 0)
						write.write(tab, 0, nbread);
				}
				finally
				{
					write.close();
				}
			}
			finally
			{
				read.close();
			}
		} catch (Exception e)
		{
			e.printStackTrace();
			if (tmp != null)
				tmp.delete();
			tmp = null;
		}

		return tmp;
	}

	@Override
	public String toString() {
		/*
		 * StringBuffer s=new StringBuffer(); s.append("p cnf ");
		 * s.append(String.valueOf(declaredNumVar)); s.append(" ");
		 * s.append(String.valueOf(declaredNumClause)); s.append("\n"); for(Clause cl : clauses){
		 * s.append(cl.toString()); s.append("0\n"); } return s.toString();
		 */
		// TODO
		return "FileCNF : " + CNFfile.getAbsolutePath();
	}

	@Override
	public File export(File directory) {
		String name;
		try
		{
			name = File.createTempFile(PREFIX + getFileName(), SUFFIX, directory).getName();
		} catch (IOException e)
		{
			e.printStackTrace();

			return null;
		}
		return export(name, directory);
	}

	@Override
	public void check() throws IOException {
		begin = 0;
		// File tmp = new File(CNFfile);
		if (file != null)
			try
			{
				file.close();
			} catch (IOException e1)
			{// recommence
				e1.printStackTrace();
				file = null;
				check();
			}

		file = new RandomAccessFile(CNFfile, "rw");

		InputStream in = new FileInputStream(CNFfile);
		InputStreamReader ipsr = new InputStreamReader(in);
		BufferedReader br = new BufferedReader(ipsr);

		String line;
		try
		{
			while ((line = br.readLine()) != null)
			{// lit la CNF
				begin++;
				if (line.charAt(0) == COMMENTAIRE)
					continue;
				if (line.charAt(0) == DESCRIPTION)
				{
					Scanner sc = new Scanner(line.substring(SIZE_DESCRIPTION));
					declaredNumVar = sc.nextInt();
					declaredNumClause = sc.nextInt();
					break;
				}

				throw new IOException();
			}
		} catch (IOException e)
		{
			e.printStackTrace();
			stat = null;
			throw e;
		}

		// stat = new Stat();
		// stat.setNumClause(declaredNumClause);
		// stat.setNumVar(declaredNumVar);

		if (declaredNumClause > 0)
			setOffSet(1);
	}

	@Override
	public List<Clause> getClauses() throws IOException {

		// recuperer
		List<Clause> clauses_temp = new ArrayList<Clause>();
		InputStream in = new FileInputStream(CNFfile);
		InputStreamReader ipsr = new InputStreamReader(in);
		BufferedReader br = new BufferedReader(ipsr);
		String line;
		try
		{
			while ((line = br.readLine()) != null)
			{
				int i;
				if (line.charAt(0) == 'c')
					continue;
				if (line.charAt(0) == 'p')
					continue;
				List<Literal> c = new ArrayList<Literal>();
				Scanner sc = new Scanner(line);
				while ((i = sc.nextInt()) != 0)
					c.add(new Literal(i));
				clauses_temp.add(new Clause(c));
			}
		} catch (IOException e)
		{
			e.printStackTrace();
			throw e;
		}
		finally
		{
			try
			{
				br.close();
			} catch (IOException e)
			{
				e.printStackTrace();
			}
		}
		return clauses_temp;
	}

	@Override
	public void addClause(List<Literal> cl) {
		// TODO Auto-generated method stub
	}

	@Override
	public void addClause(Clause cl) {
		// TODO Auto-generated method stub
	}

	@Override
	public Clause getClause(int i) throws IOException {
		setOffSet(i);
		Clause c = getNextClause();
		return c;
	}

	/**
	 * Return the next clause in the file.
	 * 
	 * @return the next clause.
	 * @throws IOException
	 *             if something goes wrong with the file.
	 */
	public Clause getNextClause() throws IOException {
		String line = file.readLine();

		return new Clause(line);
	}

	/**
	 * Set the position of the file pointer to the beginning of the "i" clause.
	 * 
	 * @param i
	 *            number of the clause.
	 * @throws IllegalArgumentException
	 *             i is to great <=> i>declaredNumClause.
	 * @throws IOException
	 *             problem with the cnf file.
	 */
	public void setOffSet(int i) throws IOException {
		if (i > declaredNumClause || i <= 0)
			throw new IllegalArgumentException();

		try
		{
			file.seek(0);
			int nb = 0;
			for (nb = i + begin - 1 ; nb > 0 && file.readLine() != null ; nb--)
				;
		} catch (IOException e)
		{
			e.printStackTrace();
			try
			{
				file.close();
			} catch (IOException e1)
			{
				e1.printStackTrace();
				throw e;
			}

		}

	}

	@Override
	public void checkStat() throws IOException {
		stat = new Stat(this);
	}

	@Override
	public boolean close() {
		try
		{
			file.close();
		} catch (IOException e)
		{
			e.printStackTrace();
		}

		if (modify)
			if (export(CNFfile.getName(), CNFfile.getParentFile()) == null)
				return false;
		return true;

	}

	@Override
	public void closeWithoutExport() {
		try
		{
			file.close();
		} catch (IOException e)
		{
			e.printStackTrace();
		}
	}

}
